An information-flow problem typically concerns a program that operates on data of different security levels (e.g., low and high). For purposes herein, low data are public data that may be disclosed to all principals, and high data are secret data whose access must be restricted. An information-flow policy, such as noninterference, typically requires that no information about high input data can be inferred from observing low output data. In practice, the security levels can be generalized to a lattice.
Language-based techniques have been shown promising in addressing such information-flow problems. By directly examining the program code, these techniques provide a strong guarantee on information-flow security. Nonetheless, most existing language-based information-flow techniques focus on high-level languages. They do not apply to assembly code largely due to the lack of high-level abstractions (e.g., program structures and data structures) and the extreme flexibility (e.g., memory aliasing and first-class code pointers) of assembly code.
It is useful to address information-flow problems for assembly code, because some applications are distributed (e.g., native code for mobile computation) or even directly written (e.g., embedded systems) in assembly code. A type system has been proposed in such a context. More specifically, that type system uses type annotations to restore the missing abstraction in assembly code, and uses type-preserving compilation to preserve security evidence from the source to the target. By security-type checking directly at the target level, code consumers gain confidence that the behavior of untrusted code satisfies certain desired information-flow policies.
Attackers may sometimes also be able to exploit covert information-flow channels, such as program timing behaviors. By either observing physically the execution time of a program (external timing) or exploiting thread interaction (internal timing), attackers may learn information about secret data. It is therefore useful to have a solution that protects information-flow security in the presence of such timing-related covert channels, particularly for assembly code with its lack of abstraction and extreme flexibility.
With respect to prior solutions on covert channels and multi-threading, Volpano and Smith, “Eliminating Covert Flows with Minimum Typings,” 10th IEEE Computer Security Foundations Workshop, pages 156-169, Washington, D.C., June 1997, studied termination-sensitive noninterference, and proposed a type system that closes termination channels by disallowing loops from occurring at sensitive program points. Agat, in “Transforming Out Timing Leaks,” Proc. 27th ACM Symposium on Principles of Programming Languages, pages 40-53, Boston, Mass., January 2000, used program transformation to prevent timing leaks, where the execution times of high branches are equalized by cross-padding with appropriate dummy instructions. Smith and Volpano, “Secure Information Flow in a Multi-Threaded Imperative Language,” Proc. 25th ACM Symposium on Principles of Programming Languages, pages 355-364, San Diego, Calif., January 1998, established possibilistic noninterference for a multi-threaded language by, again, disallowing loops from occurring at sensitive program points. Sabelfeld and Sands, “Probabilistic Noninterference for Multi-Thread Programs,” Proc. 13th IEEE Computer Security Foundations Workshop, pages 200-214, Cambridge, UK, July 2000, proved a probabilistic noninterference result with respect to a scheduler-independent security condition. These systems address information-flow security for source-level programs, and are not applicable to assembly code.
From the perspective of typed assembly languages, there has been some recent effort toward enforcing information-flow security directly at the target-code level. However, none of this work tackled covert channels and/or multi-threading. This presents difficulty when applying the solutions to real-world scenarios, where covert channels and threads interaction are easily exploitable.